1. Technical Field
This disclosure relates to electronic design automation (EDA). Specifically, this disclosure relates to methods and systems for performing formal equivalence checking between two models of a circuit design using checkpoints.
2. Related Art
Rapid advances in technology have made it possible to integrate complex large-scale systems onto a single semiconductor chip. In order to keep up with this rapid increase in size and complexity, circuit designers are designing hardware at increasingly higher levels of abstraction. Note that higher levels of abstraction are inherently faster to simulate. Hence, representing an IC (integrated circuit) design at a high level of abstraction facilitates performing more complex design exploration and more thorough validation. For example, some circuit design flows begin by writing an IC design specification in a high-level programming language, such as C, C++, SystemC, SystemVerilog, etc. Such high-level descriptions of the circuit design are often referred to as a high-level model (HLM) for the IC design.
In a typical design flow, the level of abstraction decreases as the circuit design progresses through the design flow. For example, a circuit design which is represented using an HLM at the beginning of the design flow may be represented using a register-transfer-level (RTL) model at a later stage in the design flow. The question of functional equivalency arises whenever the same circuit design is described at different levels of abstraction. For example, when an HLM for a circuit design is converted into an RTL model, it is important to ensure that the two models are functionally equivalent.
There are generally two approaches for checking functional equivalency between two models. The first approach is to exhaustively simulate the two models to ensure that the inputs and outputs for the two models are exactly the same under all conditions. Unfortunately, this approach is usually impractical because of the immense computational resources required to exhaustively simulate the two models. Note that, if we do not perform exhaustive simulation, we cannot guarantee functional equivalency between the two models.
The other approach uses formal verification techniques to prove that the two models are functionally equivalent. Unfortunately, this approach often runs into serious runtime and memory issues because the computational resources required to formally verify a circuit design can grow exponentially with the circuit design size.
Hence, what is needed are techniques and systems for checking equivalency between two models of a circuit design without the above-described problems.